import re
filename=str(input("Please enter a file name:"))
file=open(filename,'r',encoding='utf-8')#以utf-8格式打开，使能够显示取反的字符
num=file.readline()
num=int(num)
print(num)
#将数据存储到words的二位列表中
words=[]
for i in range(num):
    line=file.readline()
    print(line,end='')
    #如果整个为一个子句，则去掉前后的括号
    if line[0]=='(':
        line=line[1:len(line)-1]
    #讲左右括号前后都添加空格，按空格split可以让变量和谓词分离存储    
    word=line.replace('(',' ( ').replace(')',' ) ').replace(',',' ').split()
    words.append(word)
print("")
#定义归结类
class guijie:
    def __init__(self,words):
        self.words=words
        self.var_to_con={}#字典变量：记录变量和替换成的常量
        self.resolve_num=0#记录有效归结的次数
    
    #提取谓词和参数(返回一个字典类型)
    def get_para(self,clause):
        dict1={}
        name=""
        para=[]
        #print(clause)
        #讲每个谓词以及对应的变量以字典的形式存储
        for atom in clause:
            if atom=='(' or atom==',':
                continue
            elif name=='':
                name=name+atom
            elif atom==')':#当前原子式已结束
                dict1[name]=para
                name=''
                para=[]
            else:
                para.append(atom)
        return dict1
                
            
    #判断两个原子公式的谓词是否相等（能否归结）
    def if_can_resolve(self,clause1,clause2):
        dict1=self.get_para(clause1)
        dict2=self.get_para(clause2)
        
        id11=0
        for name1,para1 in dict1.items():
            id11=id11+1
            id22=0
            for name2,para2 in dict2.items():
                id22=id22+1
                if (name1[0]=='¬' and name2[0]!='¬' and name1[1:]==name2) or (name1[0]!='¬' and name2[0]=='¬' and name1==name2[1:]):
                    self.var_to_con=self.MGU(para1,para2)
                    if self.var_to_con!=None:
                        return True,dict1,id11,dict2,id22
        
        return False,dict1,id11,dict2,id22
    
    #判断是否为变量
    def isvariable(self,word):
        pattern1=re.compile('[u-z]')
        pattern2=re.compile('[a-t]')
        if pattern1.search(word) and not pattern2.search(word):
            return True
        else:
            return False
    
    #判断两个原子公式中的变量能否归结
    #包括1.只有一个变量不同；2.都是常量等情况都是合理的
    def MGU(self,atom1,atom2):
        mgu={}
        can_mgu=0
        same_ele=0
        num1=0
        for ele1 in atom1:
            num1=num1+1
            num2=0
            for ele2 in atom2:
                num2=num2+1
                #如果两个位置没有对上，跳过
                if num1!=num2:
                    continue
                #如果元素相同，跳过
                if ele1==ele2:
                    same_ele=same_ele+1
                    continue
                #如果两个都是变量且不相等,返回空
                elif self.isvariable(ele1) and self.isvariable(ele2):
                    return None
                elif self.isvariable(ele1):
                    mgu[ele1]=ele2
                    can_mgu=can_mgu+1
                elif self.isvariable(ele2):
                    mgu[ele2]=ele1
                    can_mgu=can_mgu+1 
                else:
                    return None
        if can_mgu==1:
            return mgu
        elif same_ele==len(atom1):
            mgu[' ']=' '
            return mgu
        else:
            return None
        
    def change_alpha(self,num):
        letter=chr(num+96)
        return letter
    
    #实现归结的过程，并打印出归结式    
    def unity(self,dict1,id1,id11,dict2,id2,id22):
        new_clause=[]
    
        var,con=list(self.var_to_con.items())[0]
        self.var_to_con.clear()
        
        #讲变量转化成常量
        for name1,para1 in dict1.items():
            for i in range(len(para1)):
                if para1[i]==var:
                    para1[i]=con
        
        for name2,para2 in dict2.items():
            for i in range(len(para2)):
                if para2[i]==var:
                    para2[i]=con
        
        #讲互为反的原子式去除，归结的结果存入新的子句中（一个列表）
        num1=0
        for name1,para1 in dict1.items():
            num1=num1+1
            if num1!=id11:
                new_clause.append(name1)
                new_clause.append('(')
                for j in range(len(para1)):
                    new_clause.append(para1[j])
                    if j!=len(para1)-1 :
                        new_clause.append(',')
                        
                new_clause.append(")")
        
        num2=0    
        for name2,para2 in dict2.items():
            num2=num2+1
            if num2!=id22:
                new_clause.append(name2)
                new_clause.append('(')
                for j in range(len(para2)):
                    new_clause.append(para2[j])
                    if j!=len(para2)-1 :
                        new_clause.append(',')
                    
                new_clause.append(")")
                           
        #有重复归结的情况，直接跳过
        if new_clause in self.words:
            new_clause.append('x')
            return new_clause
        
        self.resolve_num=self.resolve_num+1
        #跳转至结束条件
        if var==' ' and con==' ':
            return self.specific(dict1,id1,id11,dict2,id2,id22)
        
        #打印归结过程
        new_print=''
        if len(dict1)==1 and len(dict2)==1:
                new_print='R['+str(id1)+','+str(id2)+']{'+var+'='+con+'}= '
        elif len(dict1)==1:
            new_print='R['+str(id1)+','+str(id2)+self.change_alpha(id22)+']{'+var+'='+con+'}= '
        elif len(dict2)==1:
            new_print='R['+str(id1)+self.change_alpha(id11)+','+str(id2)+']{'+var+'='+con+'}= '
        else:
            new_print='R['+str(id1)+self.change_alpha(id11)+','+str(id2)+self.change_alpha(id22)+']{'+var+'='+con+'}= '
        
        if new_clause==[]:
            print(self.resolve_num,'.',new_print,new_clause)
        else:
            print(self.resolve_num,'.',new_print,end='')
            for i in range(len(new_clause)):
                print(new_clause[i],end='')
                if new_clause[i]==')' and i!=len(new_clause)-1:
                    print(',',end='')
            print('')
        return new_clause
    
    #处理特殊情况，即常量对常量的归结    
    def specific(self,dict1,id1,id11,dict2,id2,id22):
        new_print=''
        if len(dict1)==1 and len(dict2)==1:
            new_print='R['+str(id1)+','+str(id2)+']= []'
        elif len(dict1)==1:
            new_print='R['+str(id1)+','+str(id2)+self.change_alpha(id22)+']= []'
        elif len(dict2)==1:
            new_print='R['+str(id1)+self.change_alpha(id11)+','+str(id2)+']= []'
        else:
            new_print='R['+str(id1)+self.change_alpha(id11)+','+str(id2)+self.change_alpha(id22)+']= []'
        
        print(self.resolve_num,'.',new_print)
        return []
    
    #实现一阶逻辑归结的总步骤
    def First_Order_Resolution(self):
        id1=0
        finish=False
        count=1000
        while finish!=True:
            for clause1 in self.words:
                if finish==True:
                    return
                elif count<=0:
                    print("Unable to resolve!")
                    return
                id2=0
                id1=id1+1
                for clause2 in self.words:
                    id2=id2+1
                    count=count-1
                    if clause1!=clause2:
                        isok,dict1,id11,dict2,id22=self.if_can_resolve(clause1,clause2)
                        #返回能否归结以及两个谓词以及对应的元
                        if isok==True:
                            new_clause=self.unity(dict1,id1,id11,dict2,id2,id22)
                            
                            if len(new_clause)==1 and new_clause[0]=='x':
                                continue
                            elif new_clause==[]:
                                finish=True
                                print("Successfully Resolved!")
                                return
                            else:
                                words.append(new_clause)
                        
task=guijie(words)
task.First_Order_Resolution()
file.close()